proofs(lean4): mechanize the L1/L2 core (MECH-1 totality+stability, MECH-2 complete) with hard gates#17
Merged
Merged
Conversation
…ade algebras, hard gates
MECH-2 (complete): GradeAlgebra as the ET-4 ordered-semiring law set
(16 laws as proof fields) with instances Affine {0,1,w}, tropical Cost
(min/+), the generic bounded-distributive-lattice theorem instantiated
at Level (Low<=High), and the componentwise product R x S (ET-5:
composite disciplines are composition of algebras, proven once).
MECH-1 (totality core + stability): intrinsically-kinded type-level
STLC with the Keller-Altenkirch rem/wkv/eqv toolkit; beta-normal forms
with LEFT-NESTED spines (append is cons, the spine fold is structural);
hereditary substitution + normalizer total by a (kindSize, tag, size)
lexicographic measure — the Totality Gate (ET-1) discharged by
construction. DefEq stated; stability nf_emb : nf (embNf n) = n proven.
Soundness/completeness (defEq_iff_nf, decDefEq) recorded OPEN in
PROOF-STATUS — stated, never stubbed.
Gates (wire-first, watched to fail before trusted):
- scripts/check-proofs.sh: MANIFEST-driven; absent prover = FAIL;
per-module lake build; whole-package build; mandatory axiom audit
pinned to Lean's three-axiom trusted base (a smuggled user axiom
fails the gate even though it compiles green).
- scripts/scan-dangerous.sh: comment-aware scan incl. axiom/admit/
native_decide; FIXED Lean block-comment stripping ({- -} -> /- -/).
- scripts/check-proof-status.sh: drift gate — PROOF-STATUS.adoc must
match MANIFEST ground truth or CI fails.
- .github/workflows/proofs.yml: sha-pinned actions, elan 4.2.3 from a
checksum-verified release tarball, toolchain from lean-toolchain,
cache keyed on the toolchain pin. No floating setup actions.
All 11 modules gated; audit 12/12 within the trusted base; zero sorry,
zero user axioms. Verified failure modes: broken proof, smuggled axiom,
absent prover, unlisted file, status drift.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
hyperpolymath
added a commit
that referenced
this pull request
Jul 21, 2026
…h (PR-6, closes the sequence) (#21) Final PR of the completion sequence (#11 → #12 → #13 → #15 → #16 → #17 → this). - **STATE.a2ml** — completion 15→32 with per-phase justification comments; blockers echo #18/#19 + the anytype audit trail (anytype #13–#19, PR #20). - **AFFIRMATION.adoc** — anchor filled (main @ `a11c9877`, 2026-07-21T14:43Z, Lean 4.32.0/elan 4.2.3) in the same session that re-ran every check listed; every "affirmed-ran" row corresponds to a command actually executed. NOT-claims list keeps ET-2 closure, ET-6..9, ET-10..13, ET-14 explicitly open. - **Justfile** — `test`/`lint`/`fmt-check` were template echo-stubs (fake green). Now: `test` = proof gate + drift gate; `lint` = dangerous-construct scan, md-in-docs, root-shape, template validation; `fmt-check` honestly reports that nothing is checked. `check-no-vlang.sh` deferred to #19 (tracked, not silently skipped). `.machine_readable/root-allow.txt` updated for root entries landed by #14/#17. - **README** — badge `theory_(no_proofs_yet)` → `theory_(L2_proven, L1_core_proven, rest_OPEN)`; Status section states precisely what is machine-checked vs open. Verification (all run in this session at the anchor SHA): `./scripts/check-proofs.sh lean4` PASS (audit 12/12); `./scripts/scan-dangerous.sh` PASS; `./scripts/check-proof-status.sh` PASS; `./scripts/validate-template.sh` PASS (4 warnings); `just test && just quality` PASS end-to-end. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
PR-5 of the completion sequence (#11 → #12 → #13 → #15 → #16 → this).
What is proven (all under Lean 4.32.0, hermetic, no mathlib, no
sorry, no user axioms)MECH-2 — complete.
Systemet.L2.GradeAlgebrais the precise ET-4 statement: an ordered-semiring law set whose 16 fields are the proof obligations. Instances:Affine{0,1,ω}, tropicalCost(min/+, ∞ identity), the generic theorem that every bounded distributive lattice is a grade algebra (instantiated atLevel= Low≤High), and the componentwise productR × S— ET-5's "same rules, different algebra", proven once.MECH-1 — totality core + stability. Intrinsically-kinded type-level STLC (Keller–Altenkirch toolkit); β-normal forms with left-nested spines; hereditary substitution and the normalizer are total by a
(kindSize, tag, size)lexicographic measure — the Totality Gate (ET-1) discharged by construction.DefEqstated; stabilitynf_emb : nf (embNf n) = nproven. Soundness/completeness (defEq_iff_nf,decDefEq) are OPEN, stated inConversion.lean's docstring and PROOF-STATUS — never stubbed.Gates (wire-first; every one watched to fail before its green was trusted)
check-proofs.sh lean4— MANIFEST-driven, absent prover = FAIL, per-module + package buildSystemet/Audit.lean, 12#print axioms) pinned to the three-axiom trusted baseaxiom cheat : Falsecompiles green and still fails the gate, named in outputscan-dangerous.sh(comment-aware; incl.axiom/admit/native_decide){- -}→/- -/) — was false-positive-prone; canary-tested both directionscheck-proof-status.sh— PROOF-STATUS.adoc must match MANIFEST countsCI (
proofs.yml): sha-pinnedactions/checkout+actions/cache, elan 4.2.3 from a checksum-verified release tarball, toolchain from the committedlean-toolchain, cache keyed on that pin. Note: the sha9c091bb2…used across this repo's workflows is actually v7.0.0 (some existing comments mislabel it v6.0.1).Honesty ledger
lake buildclean, audit 12/12, drift gate PASS.🤖 Generated with Claude Code